\begin{tabbing}
$\forall$${\it the\_es}$:ES.
\\[0ex](Trans $e$,${\it e'}$:E. ($e$ $<$loc ${\it e'}$))
\\[0ex]\& SWellFounded(($e$ $<$loc ${\it e'}$))
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E. loc($e$) $=$ loc(${\it e'}$) $\in$ Id $\Leftrightarrow$ ($e$ $<$loc ${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ $\vee$ (${\it e'}$ $<$loc $e$))
\\[0ex]\& ($\forall$$e$:E. first($e$) $\Leftrightarrow$ ($\forall$${\it e'}$:E. $\neg$(${\it e'}$ $<$loc $e$)))
\\[0ex]\& ($\forall$$e$:E. $\neg$first($e$) $\Rightarrow$ (pred($e$) $<$loc $e$) \& ($\forall$${\it e'}$:E. $\neg$((pred($e$) $<$loc ${\it e'}$) \& (${\it e'}$ $<$loc $e$))))
\\[0ex]\& ($\forall$$e$:E. $\neg$first($e$) $\Rightarrow$ ($\forall$$x$:Id. ($x$ when $e$) $=$ ($x$ after pred($e$)) $\in$ vartype(loc($e$);$x$)))
\\[0ex]\& (Trans $e$,${\it e'}$:E. ($e$ $<$ ${\it e'}$))
\\[0ex]\& SWellFounded(($e$ $<$ ${\it e'}$))
\\[0ex]\& ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ sends(lnk($e$);sender($e$))[index($e$)] $=$ msg(lnk($e$);tag($e$);val($e$)) $\in$ Msg)
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E. ($e$ $<$loc ${\it e'}$) $\Rightarrow$ ($e$ $<$ ${\it e'}$))
\\[0ex]\& ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ (sender($e$) $<$ $e$))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:E.\+
\\[0ex]($e$ $<$ ${\it e'}$)
\\[0ex]$\Rightarrow$ \=$\neg$first(${\it e'}$) \& ($e$ $<$ pred(${\it e'}$)) $\vee$ $e$ $=$ pred(${\it e'}$)\+
\\[0ex]$\vee$ isrcv(${\it e'}$) \& ($e$ $<$ sender(${\it e'}$)) $\vee$ $e$ $=$ sender(${\it e'}$))
\-\-\\[0ex]\& ($\forall$$e$:E. isrcv($e$) $\Rightarrow$ loc($e$) $=$ destination(lnk($e$)) $\in$ Id)
\\[0ex]\& ($\forall$$e$:E, $l$:IdLnk. $\neg$loc($e$) $=$ source($l$) $\in$ Id $\Rightarrow$ sends($l$;$e$) $=$ nil $\in$ (Msg on $l$) List)
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:E.\+
\\[0ex]isrcv($e$)
\\[0ex]$\Rightarrow$ isrcv(${\it e'}$)
\\[0ex]$\Rightarrow$ lnk($e$) $=$ lnk(${\it e'}$) $\in$ IdLnk
\\[0ex]$\Rightarrow$ (\=($e$ $<$loc ${\it e'}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex](sender($e$) $<$loc sender(${\it e'}$)) $\vee$ sender($e$) $=$ sender(${\it e'}$) $\in$ E \& index($e$)$<$index(${\it e'}$)))
\-\-\\[0ex]\& (\=$\forall$$e$:E, $l$:IdLnk, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$sends($l$;$e$)$\parallel$}}$.\+
\\[0ex]$\exists$${\it e'}$:E. isrcv(${\it e'}$) \& lnk(${\it e'}$) $=$ $l$ \& sender(${\it e'}$) $=$ $e$ \& index(${\it e'}$) $=$ $n$ $\in$ $\mathbb{Z}$)
\-
\end{tabbing}